#CNF Formulas:
c1 = ["and", "X10 != a1", "X6 != a2"]
c2 = ["and", "X2 = X7", "X12 = X14"]
c3 = ["and", ["or", "X17 = X4", "X12 != X11"], ["or", "X19 = X3", "X19 != X7"]]
c4 = ["and", ["or", "X10 != X16", "X13 != X18"], ["or", "X18 != X13", "X5 != X16"]]
c5 = ["and", ["or", "X13 = X3", "X14 != X18", "X1 = a3"], ["or", "X3 != X6", "X1 = a1", "X18 = X17"]]
c6 = ["and", ["or", "X1 = X18", "X11 = X17", "X15 = a2"], ["or", "X8 != X10", "X15 != X4", "X15 != X16"]]
c7 = ["and", ["or", "X18 = X1", "X19 != X11", "X4 != X11", "X20 = a5"], ["or", "X13 = a2", "X9 = X18", "X17 = X12", "X4 != X12"]]
c8 = ["and", ["or", "X1 = X9", "X9 != X16", "X8 = a4", "X6 != a1"], ["or", "X18 = X14", "X19 != X9", "X20 = a4", "X12 = X17"]]
c9 = ["and", ["or", "X11 != X18", "X5 = X12", "X14 = a4", "X3 = X12", "X3 != X19"], ["or", "X5 = a2", "X2 = X4", "X17 = X2", "X4 = a2", "X7 = X11"]]
c10 = ["and", ["or", "X7 != X9", "X11 = X6", "X1 != X3", "X16 != X4", "X6 != X5"], ["or", "X15 = X14", "X20 != X1", "X7 = X15", "X20 != X17", "X3 != X9"]]
c11 = ["and", "X13 != a2", "X3 = X19", "X20 = X4"]
c12 = ["and", "X10 != X13", "X20 != a3", "X1 = X2"]
c13 = ["and", ["or", "X11 != X3", "X10 != X3"], ["or", "X2 != X14", "X15 != X6"], ["or", "X11 = X12", "X15 != X17"]]
c14 = ["and", ["or", "X11 != X6", "X17 != a5"], ["or", "X19 = X8", "X12 = a3"], ["or", "X4 != X9", "X12 != X7"]]
c15 = ["and", ["or", "X12 != a1", "X12 = a1", "X9 = X1"], ["or", "X15 != X8", "X14 != X16", "X14 = X7"], ["or", "X10 != X15", "X19 = a4", "X17 = X19"]]
c16 = ["and", ["or", "X5 != X11", "X2 != X16", "X13 != X10"], ["or", "X8 = X1", "X11 != X13", "X5 != X3"], ["or", "X5 = X9", "X14 = X13", "X13 = X5"]]
c17 = ["and", ["or", "X18 = X6", "X2 != X12", "X14 = X15", "X7 != X10"], ["or", "X12 != X14", "X16 = X19", "X7 != X6", "X11 = X4"], ["or", "X2 != a4", "X7 != a4", "X4 != X2", "X3 = X15"]]
c18 = ["and", ["or", "X14 != X7", "X7 != a1", "X19 != X16", "X9 != X4"], ["or", "X19 != X1", "X11 != X18", "X15 = X1", "X19 = X6"], ["or", "X4 != a2", "X16 = X2", "X14 != a4", "X10 != X20"]]
c19 = ["and", ["or", "X12 != X4", "X14 = a3", "X4 != X13", "X10 != X3", "X20 != X9"], ["or", "X18 != a3", "X4 = a2", "X12 != a4", "X15 != X11", "X14 = X2"], ["or", "X19 != X4", "X5 = X3", "X16 != a1", "X20 != X13", "X19 = a3"]]
c20 = ["and", ["or", "X6 != a1", "X1 != X3", "X8 = X16", "X4 = X3", "X11 != X6"], ["or", "X9 != X2", "X17 != X19", "X16 != X5", "X16 = X2", "X19 = X11"], ["or", "X12 != X18", "X4 = X3", "X19 = X20", "X1 != X16", "X10 = a4"]]
c21 = ["and", "X12 != X17", "X12 = X14", "X2 != X5", "X20 != a1"]
c22 = ["and", "X11 != X4", "X19 != X10", "X7 = X6", "X10 != X7"]
c23 = ["and", ["or", "X16 = X18", "X9 != X17"], ["or", "X7 != X13", "X13 = X15"], ["or", "X3 = X6", "X15 = a4"], ["or", "X14 != X12", "X12 != X8"]]
c24 = ["and", ["or", "X2 != a1", "X5 != a1"], ["or", "X13 != X18", "X8 = X18"], ["or", "X14 != X10", "X17 = X10"], ["or", "X6 != X11", "X8 != a5"]]
c25 = ["and", ["or", "X2 != X17", "X15 != X10", "X19 = X7"], ["or", "X17 = X20", "X15 != X19", "X19 = X10"], ["or", "X3 = X2", "X1 = X9", "X9 = X2"], ["or", "X19 != X12", "X10 = X6", "X19 = X5"]]
c26 = ["and", ["or", "X11 != a3", "X15 = X11", "X2 = X18"], ["or", "X5 = X7", "X11 = a5", "X14 != X10"], ["or", "X1 = X14", "X3 = X6", "X8 = X5"], ["or", "X4 != X5", "X9 = X2", "X8 != X15"]]
c27 = ["and", ["or", "X9 != X6", "X16 != X6", "X12 != X13", "X20 != X4"], ["or", "X20 != X1", "X4 != X18", "X15 != X4", "X3 = X4"], ["or", "X4 = X5", "X14 = X2", "X20 = a1", "X16 != a5"], ["or", "X5 != X2", "X14 = X10", "X14 != X18", "X14 != X16"]]
c28 = ["and", ["or", "X17 = X4", "X17 = a5", "X12 = X5", "X6 != X3"], ["or", "X15 != X5", "X16 != X20", "X15 != X11", "X12 != X15"], ["or", "X10 = a4", "X11 = X8", "X18 = X12", "X20 = a5"], ["or", "X8 = X10", "X4 != X5", "X1 = X12", "X1 != X17"]]
c29 = ["and", ["or", "X1 = a4", "X13 = X6", "X15 = X4", "X1 = X12", "X10 != X20"], ["or", "X16 = a2", "X20 = X9", "X7 != X16", "X10 != X3", "X19 != X10"], ["or", "X5 = X13", "X17 != a3", "X18 != X16", "X15 = a2", "X19 != a5"], ["or", "X2 != X16", "X14 != X15", "X1 = X7", "X4 != a4", "X17 = X20"]]
c30 = ["and", ["or", "X10 = X1", "X12 != X13", "X6 = a1", "X18 = X20", "X14 = X12"], ["or", "X10 != X8", "X16 = a3", "X3 = X4", "X20 = X7", "X12 = X1"], ["or", "X12 != X1", "X19 = X11", "X9 != X17", "X8 != X1", "X18 = a3"], ["or", "X16 != X20", "X4 = X11", "X16 = a1", "X9 != X20", "X14 != a2"]]
c31 = ["and", "X20 != X9", "X13 != X6", "X3 = X16", "X20 != X9", "X7 = X9"]
c32 = ["and", "X5 != X7", "X17 != a5", "X19 = X3", "X1 != X19", "X18 = X16"]
c33 = ["and", ["or", "X5 = X7", "X10 != X3"], ["or", "X17 != X5", "X6 != X5"], ["or", "X14 != X18", "X7 != X16"], ["or", "X7 != X8", "X7 = X4"], ["or", "X8 != a5", "X3 = X2"]]
c34 = ["and", ["or", "X6 != X19", "X18 = X3"], ["or", "X9 = X18", "X20 != X18"], ["or", "X19 = a5", "X10 = X19"], ["or", "X7 = a3", "X20 != X2"], ["or", "X16 != X9", "X5 = X6"]]
c35 = ["and", ["or", "X5 = X12", "X2 != X13", "X13 = X12"], ["or", "X18 != X6", "X16 != X15", "X17 != a3"], ["or", "X12 = X11", "X14 != X13", "X9 != X19"], ["or", "X10 = X13", "X4 = X11", "X11 != X14"], ["or", "X4 != X11", "X1 = X13", "X19 = X16"]]
c36 = ["and", ["or", "X17 = a2", "X10 != a1", "X7 = X5"], ["or", "X20 = a2", "X9 = X19", "X9 != X11"], ["or", "X17 = X5", "X18 = X9", "X10 != X13"], ["or", "X18 != X16", "X3 != X2", "X8 != X1"], ["or", "X13 = X11", "X3 != X5", "X20 = X8"]]
c37 = ["and", ["or", "X5 != a1", "X7 != X12", "X6 = X19", "X11 != X13"], ["or", "X2 = X15", "X4 != X18", "X17 != X11", "X13 != X4"], ["or", "X1 = X20", "X15 = X12", "X1 = a5", "X7 != a2"], ["or", "X13 != a2", "X7 != X19", "X11 != X14", "X12 != X16"], ["or", "X9 = X15", "X6 = X2", "X5 = X16", "X4 != X5"]]
c38 = ["and", ["or", "X9 != X12", "X3 != X19", "X19 != X6", "X13 = X1"], ["or", "X1 = X16", "X14 != X8", "X16 = X7", "X10 != a1"], ["or", "X13 != X7", "X17 != X5", "X18 != X5", "X5 = X1"], ["or", "X3 = X10", "X10 != X3", "X1 != X12", "X6 != a3"], ["or", "X20 != X4", "X13 = X19", "X16 != X2", "X5 = a3"]]
c39 = ["and", ["or", "X12 = a2", "X13 = X3", "X1 != a3", "X6 = a5", "X9 != X18"], ["or", "X8 != X11", "X12 = X7", "a5 = X5", "X2 = X19", "X5 = X17"], ["or", "X15 != a2", "X16 = X9", "X4 != X20", "X15 = X4", "X17 != X15"], ["or", "X14 != X13", "X10 = X16", "X19 != X10", "X20 = X5", "X8 != a3"], ["or", "X2 != a3", "X3 != X15", "X19 = X16", "X1 = X15", "X1 != a2"]]
c40 = ["and", ["or", "X11 != X14", "X16 != X5", "X10 != X1", "X14 != a2", "X18 = a4"], ["or", "a2 = X8", "X19 = X12", "X2 = X20", "X16 != a2", "X5 = X16"], ["or", "X13 != X10", "X6 != a1", "X4 != X17", "X6 = X2", "X4 != X1"], ["or", "X20 != X12", "X14 != X19", "X1 = X19", "X13 != a1", "X9 = X17"], ["or", "X15 = a5", "X12 != X11", "X12 = X8", "X2 = a4", "X16 = X12"]]

cnf_formulas = [c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30, c31, c32,c33, c34, c35, c36, c37, c38, c39, c40]

#DNF formulas
d1 = ["or", "X1 = X15", "X4 != X12"]
d2 = ["or", "X5 = X20", "X7 != X4"]
d3 = ["or", ["and", "X6 = X19", "X6 = X4"], ["and", "X1 != X10", "X6 != X20"]]
d4 = ["or", ["and", "X11 = X15", "X12 = X6"], ["and", "X19 = X16", "X19 != X6"]]
d5 = ["or", ["and", "X5 = a3", "X17 = X4", "X9 != X2"], ["and", "X2 != a5", "X7 != X6", "X11 != X14"]]
d6 = ["or", ["and", "X11 = X19", "X3 = a4", "X13 = X6"], ["and", "X11 != X14", "X2 != X16", "X6 = X16"]]
d7 = ["or", ["and", "X11 = a3", "X4 = X15", "X3 = X2", "X2 != a2"], ["and", "X14 = a4", "X13 != X2", "X18 != X15", "X1 != a2"]]
d8 = ["or", ["and", "X10 != a5", "X18 = a4", "X8 = X11", "X15 = X20"], ["and", "X18 != X6", "X20 != X13", "X15 != X16", "X17 = X2"]]
d9 = ["or", ["and", "X8 = X16", "X17 = X19", "X18 != X11", "X2 != a1", "X18 != X5"], ["and", "X6 = a4", "X20 = X10", "X7 = a4", "X9 != X13", "X2 = X19"]]
d10 = ["or", ["and", "X2 != X17", "X3 != X14", "X15 != X7", "X13 = X10", "X11 = a5"], ["and", "X18 != X10", "X1 = X9", "X8 != X17", "X15 = X3", "X14 = X8"]]
d11 = ["or", "X18 != X17", "X17 = a4", "X19 != X16"]
d12 = ["or", "X13 = X6", "X16 = a2", "X20 != X2"]
d13 = ["or", ["and", "X8 = X4", "X7 = X13"], ["and", "X20 != X6", "X19 = X10"], ["and", "X10 = X12", "X10 != X16"]]
d14 = ["or", ["and", "X11 != X7", "X11 != X16"], ["and", "X13 = X10", "X16 != a5"], ["and", "X7 = X12", "X8 = a4"]]
d15 = ["or", ["and", "X5 = X13", "X20 != X6", "X18 = X7"], ["and", "X20 = X16", "X17 != X10", "X10 != X14"], ["and", "X13 != X6", "X16 = X19", "X13 = X1"]]
d16 = ["or", ["and", "X7 = a1", "X12 != a3", "X2 = a2"], ["and", "X14 != X8", "X1 != X9", "X16 != X3"], ["and", "X2 != X20", "X8 = X1", "X5 != X20"]]
d17 = ["or", ["and", "X2 = a1", "X13 = a2", "X18 != X16", "X18 = X16"], ["and", "X13 != a2", "X13 != X4", "X19 = X8", "X12 != X3"], ["and", "X2 != X11", "X11 != a5", "X2 = X8", "X15 = X8"]]
d18 = ["or", ["and", "X5 = X8", "X20 != X15", "X11 != X16", "X8 != X19"], ["and", "X16 = X1", "X11 != X9", "X7 != a1", "X7 = a5"], ["and", "X19 = X15", "X5 != X1", "X5 = X6", "X11 = X8"]]
d19 = ["or", ["and", "X5 = X16", "a1 != X12", "X6 != X3", "X18 != X10", "X3 != X14"], ["and", "X15 = a3", "X6 != X1", "X7 != a2", "X14 = X10", "X18 = X2"], ["and", "X4 = X6", "X5 != X16", "X9 = X5", "X2 != a3", "X12 = X3"]]
d20 = ["or", ["and", "X7 != a4", "X19 != X5", "X5 != a1", "X17 != a2", "X1 != X7"], ["and", "X8 != X11", "X11 != a1", "X10 != X1", "X15 != X4", "X2 != X17"], ["and", "X14 = X12", "X13 != a1", "X20 != X9", "X7 != a2", "X6 = X10"]]
d21 = ["or", "X4 != X7", "X9 = X7", "X8 != a4", "X14 = X9"]
d22 = ["or", "X10 != X15", "X1 != X18", "X4 != X10", "X16 = X5"]
d23 = ["or", ["and", "X19 != X6", "X11 != a1"], ["and", "X2 != X16", "X13 != X4"], ["and", "X6 != a5", "X12 != X11"], ["and", "X10 != a5", "X5 != X12"]]
d24 = ["or", ["and", "X15 = X19", "X15 = X7"], ["and", "X6 != X18", "X13 != X4"], ["and", "X18 = a4", "X15 != X17"], ["and", "X9 != X14", "X1 = X6"]]
d25 = ["or", ["and", "X17 = X5", "X16 = X7", "X2 = X15"], ["and", "X14 = X5", "X19 = X17", "X1 = X20"], ["and", "X6 != X9", "X6 != X14", "X2 = X10"], ["and", "X1 != X12", "X8 != X17", "X10 != X12"]]
d26 = ["or", ["and", "X7 = a1", "X11 = X12", "X3 = X19"], ["and", "X4 = a5", "X17 = X10", "X13 = X12"], ["and", "X8 != a1", "X16 != a1", "X7 = a1"], ["and", "X8 = X18", "X14 = X20", "X5 = X1"]]
d27 = ["or", ["and", "X5 != X17", "X17 = X7", "X8 = a2", "X1 != X7"], ["and", "X16 = X20", "X4 != X19", "X14 != a3", "X5 != X4"], ["and", "X9 != X19", "X19 = X13", "X19 = a5", "X3 != X13"], ["and", "X3 != X2", "X19 = X17", "X14 != a3", "X8 = X11"]]
d28 = ["or", ["and", "X12 = X3", "X17 = X20", "X3 != X7", "X13 = X12"], ["and", "X5 = X13", "X14 != X8", "X15 = a5", "X7 != X9"], ["and", "X4 != a1", "X5 != X11", "X17 = X19", "X7 = X19"], ["and", "X2 = X1", "X20 = X19", "X14 != X20", "X16 != X4"]]
d29 = ["or", ["and", "X18 != X9", "X10 = X5", "X3 != X17", "X17 = X19", "X11 = X3"], ["and", "X11 != X8", "X14 = X12", "X3 = X19", "X17 = X10", "X15 != a2"], ["and", "X7 = X10", "X18 = X11", "X3 = X17", "X3 != X1", "X10 = X4"], ["and", "X20 = X18", "X8 = X2", "X8 = a2", "X1 = X18", "X4 = X15"]]
d30 = ["or", ["and", "X7 != X6", "X14 != a3", "X13 = X7", "X8 = X3", "X16 != a4"], ["and", "X7 = X15", "X18 = a1", "X16 = X2", "X5 != X11", "X4 = X19"], ["and", "X7 = a5", "X17 = X9", "X20 != a1", "X14 = X7", "X14 = X8"], ["and", "X13 = X6", "X10 != a3", "X16 = a5", "X1 = X9", "X11 != X14"]]
d31 = ["or", "X17 != X2", "X9 != X12", "X15 = a5", "X16 = X1", "X9 != X11"]
d32 = ["or", "X12 != a5", "X10 != X20", "X16 != X1", "X14 = X11", "X14 = X4"]
d33 = ["or", ["and", "X18 = X9", "X18 = a4"], ["and", "X19 != X8", "X3 = X15"], ["and", "X9 = X11", "X10 = X1"], ["and", "X14 != X20", "X20 != a1"], ["and", "X6 = a5", "X16 = a2"]]
d34 = ["or", ["and", "X16 != X4", "X13 = X4"], ["and", "X12 = X18", "X3 = X9"], ["and", "X8 != a2", "X8 = X12"], ["and", "X3 != X11", "X9 != X16"], ["and", "X9 = X13", "X17 != X4"]]
d35 = ["or", ["and", "X3 = X7", "X17 = X4", "X13 != X20"], ["and", "X2 != X19", "X7 != a1", "X6 != X7"], ["and", "X7 != a4", "X20 != X14", "X16 = X19"], ["and", "X14 != X3", "X11 = a4", "X8 != X7"], ["and", "X10 != X17", "X5 != X10", "X11 = a5"]]
d36 = ["or", ["and", "X2 = a1", "X14 != X2", "X19 != X20"], ["and", "X18 = X9", "X16 != X10", "X11 != X4"], ["and", "X10 = X15", "X6 = a4", "X16 != X17"], ["and", "X10 != X5", "X19 != X5", "X11 != a5"], ["and", "X18 != X2", "X7 != X10", "X20 != X18"]]
d37 = ["or", ["and", "X4 = X20", "X9 != X11", "X12 = a1", "X18 != X5"], ["and", "X5 = X10", "X12 != X11", "X18 = a4", "X18 = X5"], ["and", "X2 != a3", "X6 = X2", "X2 != a3", "X20 = X3"], ["and", "X14 = X9", "X19 != X17", "X12 != X11", "X17 != a5"], ["and", "X10 != X2", "X7 = X10", "X17 = X1", "X10 != a3"]]
d38 = ["or", ["and", "X2 = X1", "X12 = X7", "X17 = X9", "X11 = a2"], ["and", "X6 != X3", "X4 != a2", "X2 = X15", "X14 != a5"], ["and", "X12 != X16", "X4 != X10", "X3 != X7", "X9 = X15"], ["and", "X20 != X16", "X15 != X16", "X1 = X16", "X6 = a4"], ["and", "X1 != X5", "X5 = X12", "X6 = a5", "X20 = X10"]]
d39 = ["or", ["and", "X3 != a3", "X14 != a1", "X5 = a3", "X7 = a3", "X1 = X7"], ["and", "X17 != a4", "X7 != X1", "X9 != X12", "X12 = X2", "X2 != X18"], ["and", "X6 != X17", "X14 = X6", "X18 = X16", "a5 != X4", "X6 != X18"], ["and", "a2 = X9", "X18 != X10", "X7 != a1", "X2 = X11", "X10 = a3"], ["and", "X5 != a3", "X13 != X3", "X13 != X11", "X3 = a2", "X18 != a1"]]
d40 = ["or", ["and", "X14 != X5", "X4 = a2", "X18 = a3", "X16 != X18", "X17 = X16"], ["and", "X12 = a3", "X18 != a3", "X20 != X15", "X9 = X2", "X11 != X1"], ["and", "X14 != X12", "X1 = X19", "X15 = X1", "X15 != X7", "X1 = X10"], ["and", "X18 = a3", "X10 != a3", "X17 = a3", "X13 = X19", "X9 != X20"], ["and", "X15 = X16", "X1 != X6", "X18 = a1", "X16 = X14", "X17 = X1"]]

dnf_formulas = [d1, d2,  d3,  d4,  d5,  d6,  d7,  d8,  d9,  d10,  d11,  d12,  d13,  d14,  d15,  d16,  d17,  d18,  d19,  d20,  d21,  d22,  d23,  d24,  d25,  d26,  d27,  d28,  d29,  d30,  d31,  d32, d33, d34, d35, d36, d37, d38, d39, d40]

m1 = ["or", "X1=X2", "X1=a1"]
dnf_formulas = [m1, ]